T:Type, f:(TT). retraction(T;f)  (x, y:T. Dec(x = y))  (x, y:T. Dec(x is f*(y))) 

latex

Definitions	t  T, s = t, , x:AB(x), x:A. B(x), Dec(P), Type, retraction(T;f), y is f*(x), P  Q, x:A  B(x), x:A. B(x), f(a), a < b, , , left + right, P  Q, #$n, n - m, {x:A| B(x)} , A  B, i  j , False, A, -n, n+m, Void, <a, b>, , |g|, S  T, {T}, hd(l), y=f*(x) via L
Lemmas	member wf, le wf, fun-connected-step-back, fun-connected-step, fun-connected transitivity, fun-connected-fixedpoint, false wf, fun-connected weakening eq, not wf, ge wf, nat properties, nat wf, nat ind tp, retraction wf, fun-connected wf, decidable wf